In this short paper, we present our ongoing work on the veriFIRE project -- a collaboration between industry and academia, aimed at using verification for increasing the reliability of a real-world, safety-critical system. The system we target is an airborne platform for wildfire detection, which incorporates two deep neural networks. We describe the system and its properties of interest, and discuss our attempts to verify the system's consistency, i.e., its ability to continue and correctly classify a given input, even if the wildfire it describes increases in intensity. We regard this work as a step towards the incorporation of academic-oriented verification tools into real-world systems of interest.

随着深度学习在关键任务系统中的越来越多的应用，越来越需要对神经网络的行为进行正式保证。确实，最近提出了许多用于验证神经网络的方法，但是这些方法通常以有限的可伸缩性或不足的精度而挣扎。许多最先进的验证方案中的关键组成部分是在网络中可以为特定输入域获得的神经元获得的值计算下限和上限 - 并且这些界限更紧密，验证的可能性越大，验证的可能性就越大。成功。计算这些边界的许多常见算法是符号结合传播方法的变化。其中，利用一种称为后替代的过程的方法特别成功。在本文中，我们提出了一种使背部替代产生更严格的界限的方法。为了实现这一目标，我们制定并最大程度地减少背部固定过程中发生的不精确错误。我们的技术是一般的，从某种意义上说，它可以将其集成到许多现有的符号结合的传播技术中，并且只有较小的修改。我们将方法作为概念验证工具实施，并且与执行背部替代的最先进的验证者相比，取得了有利的结果。

随着神经网络作为任务至关重要系统中组成部分的越来越多的整合，越来越需要确保它们满足各种安全性和livesice要求。近年来，已经提出了许多声音和完整的验证方法，但这些方法通常受到严重的可伸缩性限制。最近的工作提出了通过抽象 - 再填充功能增强这种验证技术的增强，这些功能已被证明可以提高可伸缩性：而不是验证大型且复杂的网络，而是验证者构造，然后验证一个较小的网络，其正确性意味着原始的正确性网络。这种方案的缺点是，如果验证较小的网络失败，则验证者需要执行改进步骤，以增加验证网络的大小，然后开始从SCRATCH验证新网络 - 有效地``'浪费''它的早期工作在验证较小的网络方面。在本文中，我们通过使用\ emph {残留推理}来提高基于抽象的神经网络验证的增强：在验证抽象网络时使用信息的过程，以加快对精制网络的验证。本质上，该方法允许验证者存储有关确保正确行为的搜索空间部分的信息，并允许其专注于可能发现错误的区域。我们实施了我们的方法，以扩展到Marabou验证者，并获得了有希望的结果。

深厚的增强学习（DRL）在各种机器人应用中取得了突破性的成功。自然的结果是采用这种范式来进行关键的任务，其中可以涉及人类安全和昂贵的硬件。在这种情况下，至关重要的是优化基于DRL的代理的性能，同时提供其行为的保证。本文提出了一种新型技术，用于将域专家知识纳入受约束的DRL训练环中。我们的技术利用了基于方案的编程范式，该范式旨在以简单而直观的方式指定此类知识。我们验证了有关流行的机器人地图导航问题，模拟和实际平台的方法。我们的实验表明，使用我们的方法利用专家知识极大地提高了代理的安全性和性能。

深度神经网络（DNN）越来越多地用于安全至关重要的系统中，迫切需要保证其正确性。因此，验证社区设计了多种技术和工具来验证DNN。当DNN验证者发现触发错误的输入时，很容易确认；但是，当他们报告不存在错误时，就无法确保验证工具本身没有缺陷。由于在DNN验证工具中已经观察到了多个错误，因此这将DNN验证的适用性提出了质疑。在这项工作中，我们提出了一种具有证明生产能力的基于简单的DNN验证符的新型机制：产生易于检查的不可满足性的见证人，这证明了没有错误的情况。我们的证明生产是基于众所周知的Farkas引理的有效适应，并结合了处理分段线性函数和数值精确误差的机制。作为概念的证明，我们在Marabou DNN验证者之上实施了我们的技术。我们对避免空中碰撞的安全至关重要系统的评估表明，在几乎所有情况下，证明生产都成功了，只需要最小的开销。

深度神经网络（DNN）已成为实现各种复杂任务的首选技术。但是，正如许多最近的研究所强调的那样，即使是对正确分类的输入的不可察觉的扰动也可能导致DNN错误分类。这使DNNS容易受到攻击者的战略输入操作，并且对环境噪声过敏。为了减轻这种现象，从业人员通过DNNS的“合奏”进行联合分类。通过汇总不同单个DNN的分类输出对相同的输入，基于合奏的分类可以减少因任何单个DNN的随机训练过程的特定实现而导致错误分类的风险。但是，DNN集合的有效性高度依赖于其成员 *在许多不同的输入上没有同时错误 *。在本案例研究中，我们利用DNN验证的最新进展，设计一种方法来识别一种合奏组成，即使输入对对抗性进行了扰动，也不太容易出现同时误差 - 从而导致基于更坚固的集合分类。我们提出的框架使用DNN验证器作为后端，并包括启发式方法，有助于降低直接验证合奏的高复杂性。从更广泛的角度来看，我们的工作提出了一个新颖的普遍目标，以实现正式验证，该目标可能可以改善各种应用领域的现实世界中基于深度学习的系统的鲁棒性。

由于它们在计算机视觉，图像处理和其他人领域的优异性能，卷积神经网络具有极大的普及。不幸的是，现在众所周知，卷积网络通常产生错误的结果 - 例如，这些网络的输入的小扰动可能导致严重的分类错误。近年来提出了许多验证方法，以证明没有此类错误，但这些通常用于完全连接的网络，并且在应用于卷积网络时遭受加剧的可扩展性问题。为了解决这一差距，我们在这里介绍了CNN-ABS框架，特别是旨在验证卷积网络。 CNN-ABS的核心是一种抽象细化技术，它通过拆除卷积连接，以便在这种方式创造原始问题的过度逼近来简化验证问题;如果产生的问题变得过于抽象，它会恢复这些连接。 CNN-ABS旨在使用现有的验证引擎作为后端，我们的评估表明它可以显着提高最先进的DNN验证引擎的性能，平均降低运行时间15.7％。

神经网络模型已成为各种任务的领先解决方案，例如分类，语言处理，蛋白质折叠等。但是，它们的可靠性受到对抗输入的严重困扰：导致模型产生错误输出的小输入扰动。当系统的环境随机行为，即使在没有恶意的对手的情况下，对抗性输入也可以自然发生，并且在尝试在关键系统中部署神经网络时是严重关注的原因。在本文中，我们提出了一种称为鲁棒性测量和评估（ROMA）的新统计方法，该方法可以衡量神经网络模型的预期鲁棒性。具体而言，罗姆人确定随机输入扰动可能导致错误分类的概率。该方法使我们能够就部署后训练有素的模型会遇到的预期错误的预期频率提供正式的保证。我们的方法可以应用于大规模的黑盒神经网络，与最近提出的验证方法相比，这是一个重要的优势。我们以两种方式运用我们的方法：比较不同模型的鲁棒性，并测量模型的鲁棒性如何受到输入扰动的幅度影响。通过这项工作获得的一个有趣的见解是，在分类网络中，不同的输出标签可以表现出非常不同的鲁棒性水平。我们称这种现象的鲁棒性。我们在分类基础上执行风险和鲁棒性评估的能力为缓解风险打开了大门，这可能是迈向关键安全应用中神经网络认证的重要一步。

神经网络在检测嘈杂数据中的模式方面非常成功，并且已成为许多领域的首选技术。但是，他们对对抗攻击的敏感性阻碍了它们的有用性。最近，已经提出了许多用于衡量和改善网络对对抗性扰动的鲁棒性的方法，并且这项不断增长的研究体现了许多明确或隐性的鲁棒性观念。这些概念之间的联系通常是微妙的，文献中缺少它们之间的系统比较。在本文中，我们开始解决这一差距，通过在网络的培训阶段，其验证和部署之后设置对网络鲁棒性作为数学属性的经验分析和评估的一般原则。然后，我们应用这些原则并进行案例研究，以展示我们一般方法的实际好处。

Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. We present a novel, scalable, and efficient technique for verifying properties of deep neural networks (or providing counter-examples). The technique is based on the simplex method, extended to handle the non-convex Rectified Linear Unit (ReLU ) activation function, which is a crucial ingredient in many modern neural networks. The verification procedure tackles neural networks as a whole, without making any simplifying assumptions. We evaluated our technique on a prototype deep neural network implementation of the next-generation airborne collision avoidance system for unmanned aircraft (ACAS Xu). Results show that our technique can successfully prove properties of networks that are an order of magnitude larger than the largest networks verified using existing methods.